home *** CD-ROM | disk | FTP | other *** search
/ Info-Mac 11 / Info-Mac_XI_Disc_1.cdr_ / Info-Mac XI Disc 1.cdr / Programs / Science & Math / MacEspresso 1.0 / espresso / irred.c < prev    next >
Encoding:
C/C++ Source or Header  |  1989-02-26  |  10.1 KB  |  432 lines  |  [TEXT/R*ch]
  1. #include "espresso.h"
  2.  
  3. static void fcube_is_covered();
  4. static void ftautology();
  5. static bool ftaut_special_cases();
  6.  
  7.  
  8. static int Rp_current;
  9.  
  10. /*
  11.  *   irredundant -- Return a minimal subset of F
  12.  */
  13.  
  14. pcover
  15. irredundant(F, D)
  16. pcover F, D;
  17. {
  18.     mark_irredundant(F, D);
  19.     return sf_inactive(F);
  20. }
  21.  
  22.  
  23. /*
  24.  *   mark_irredundant -- find redundant cubes, and mark them "INACTIVE"
  25.  */
  26.  
  27. void
  28. mark_irredundant(F, D)
  29. pcover F, D;
  30. {
  31.     pcover E, Rt, Rp;
  32.     pset p, p1, last;
  33.     sm_matrix *table;
  34.     sm_row *cover;
  35.     sm_element *pe;
  36.  
  37.     /* extract a minimum cover */
  38.     irred_split_cover(F, D, &E, &Rt, &Rp);
  39.     table = irred_derive_table(D, E, Rp);
  40.     cover = sm_minimum_cover(table, NIL(int), /* heuristic */ 1, /* debug */ 0);
  41.  
  42.     /* mark the cubes for the result */
  43.     foreach_set(F, last, p) {
  44.     RESET(p, ACTIVE);
  45.     RESET(p, RELESSEN);
  46.     }
  47.     foreach_set(E, last, p) {
  48.     p1 = GETSET(F, SIZE(p));
  49.     assert(setp_equal(p1, p));
  50.     SET(p1, ACTIVE);
  51.     SET(p1, RELESSEN);        /* for essen(), mark as rel. ess. */
  52.     }
  53.     sm_foreach_row_element(cover, pe) {
  54.     p1 = GETSET(F, pe->col_num);
  55.     SET(p1, ACTIVE);
  56.     }
  57.  
  58.     if (debug & IRRED) {
  59.     printf("# IRRED: F=%d E=%d R=%d Rt=%d Rp=%d Rc=%d Final=%d Bound=%d\n",
  60.         F->count, E->count, Rt->count+Rp->count, Rt->count, Rp->count,
  61.         cover->length, E->count + cover->length, 0);
  62.     }
  63.  
  64.     free_cover(E);
  65.     free_cover(Rt);
  66.     free_cover(Rp);
  67.     sm_free(table);
  68.     sm_row_free(cover);
  69. }
  70.  
  71. /*
  72.  *  irred_split_cover -- find E, Rt, and Rp from the cover F, D
  73.  *
  74.  *    E  -- relatively essential cubes
  75.  *    Rt  -- totally redundant cubes
  76.  *    Rp  -- partially redundant cubes
  77.  */
  78.  
  79. void
  80. irred_split_cover(F, D, E, Rt, Rp)
  81. pcover F, D;
  82. pcover *E, *Rt, *Rp;
  83. {
  84.     register pcube p, last;
  85.     register int index;
  86.     pcover R;
  87.     pcube *FD, *ED;
  88.  
  89.     /* number the cubes of F -- these numbers track into E, Rp, Rt, etc. */
  90.     index = 0;
  91.     foreach_set(F, last, p) {
  92.     PUTSIZE(p, index);
  93.     index++;
  94.     }
  95.  
  96.     *E = new_cover(10);
  97.     *Rt = new_cover(10);
  98.     *Rp = new_cover(10);
  99.     R = new_cover(10);
  100.  
  101.     /* Split F into E and R */
  102.     FD = cube2list(F, D);
  103.     foreach_set(F, last, p) {
  104.     if (cube_is_covered(FD, p)) {
  105.         R = sf_addset(R, p);
  106.     } else {
  107.         *E = sf_addset(*E, p);
  108.     }
  109.     if (debug & IRRED1) {
  110.         (void) printf("IRRED1: zr=%d ze=%d to-go=%d time=%s\n",
  111.         R->count, (*E)->count, F->count - (R->count + (*E)->count),
  112.         print_time(ptime()));
  113.     }
  114.     }
  115.     free_cubelist(FD);
  116.  
  117.     /* Split R into Rt and Rp */
  118.     ED = cube2list(*E, D);
  119.     foreach_set(R, last, p) {
  120.     if (cube_is_covered(ED, p)) {
  121.         *Rt = sf_addset(*Rt, p);
  122.     } else {
  123.         *Rp = sf_addset(*Rp, p);
  124.     }
  125.     if (debug & IRRED1) {
  126.         (void) printf("IRRED1: zr=%d zrt=%d to-go=%d time=%s\n",
  127.         (*Rp)->count, (*Rt)->count,
  128.         R->count - ((*Rp)->count +(*Rt)->count), print_time(ptime()));
  129.     }
  130.     }
  131.     free_cubelist(ED);
  132.  
  133.     free_cover(R);
  134. }
  135.  
  136. /*
  137.  *  irred_derive_table -- given the covers D, E and the set of
  138.  *  partially redundant primes Rp, build a covering table showing
  139.  *  possible selections of primes to cover Rp.
  140.  */
  141.  
  142. sm_matrix *
  143. irred_derive_table(D, E, Rp)
  144. pcover D, E, Rp;
  145. {
  146.     register pcube last, p, *list;
  147.     sm_matrix *table;
  148.     int size_last_dominance, i;
  149.  
  150.     /* Mark each cube in DE as not part of the redundant set */
  151.     foreach_set(D, last, p) {
  152.     RESET(p, REDUND);
  153.     }
  154.     foreach_set(E, last, p) {
  155.     RESET(p, REDUND);
  156.     }
  157.  
  158.     /* Mark each cube in Rp as partially redundant */
  159.     foreach_set(Rp, last, p) {
  160.     SET(p, REDUND);             /* belongs to redundant set */
  161.     }
  162.  
  163.     /* For each cube in Rp, find ways to cover its minterms */
  164.     list = cube3list(D, E, Rp);
  165.     table = sm_alloc();
  166.     size_last_dominance = 0;
  167.     i = 0;
  168.     foreach_set(Rp, last, p) {
  169.     Rp_current = SIZE(p);
  170.     fcube_is_covered(list, p, table);
  171.     RESET(p, REDUND);    /* can now consider this cube redundant */
  172.     if (debug & IRRED1) {
  173.         (void) printf("IRRED1: %d of %d to-go=%d, table=%dx%d time=%s\n",
  174.         i, Rp->count, Rp->count - i,
  175.         table->nrows, table->ncols, print_time(ptime()));
  176.     }
  177.     /* try to keep memory limits down by reducing table as we go along */
  178.     if (table->nrows - size_last_dominance > 1000) {
  179.         (void) sm_row_dominance(table);
  180.         size_last_dominance = table->nrows;
  181.         if (debug & IRRED1) {
  182.         (void) printf("IRRED1: delete redundant rows, now %dx%d\n",
  183.             table->nrows, table->ncols);
  184.         }
  185.     }
  186.     i++;
  187.     }
  188.     free_cubelist(list);
  189.  
  190.     return table;
  191. }
  192.  
  193. /* cube_is_covered -- determine if a cubelist "covers" a single cube */
  194. bool
  195. cube_is_covered(T, c)
  196. pcube *T, c;
  197. {
  198.     return tautology(cofactor(T,c));
  199. }
  200.  
  201.  
  202.  
  203. /* tautology -- answer the tautology question for T */
  204. bool
  205. tautology(T)
  206. pcube *T;         /* T will be disposed of */
  207. {
  208.     register pcube cl, cr;
  209.     register int best, result;
  210.     static int taut_level = 0;
  211.  
  212.     if (debug & TAUT) {
  213.     debug_print(T, "TAUTOLOGY", taut_level++);
  214.     }
  215.  
  216.     if ((result = taut_special_cases(T)) == MAYBE) {
  217.     cl = new_cube();
  218.     cr = new_cube();
  219.     best = binate_split_select(T, cl, cr, TAUT);
  220.     result = tautology(scofactor(T, cl, best)) &&
  221.          tautology(scofactor(T, cr, best));
  222.     free_cubelist(T);
  223.     free_cube(cl);
  224.     free_cube(cr);
  225.     }
  226.  
  227.     if (debug & TAUT) {
  228.     printf("exit TAUTOLOGY[%d]: %s\n", --taut_level, print_bool(result));
  229.     }
  230.     return result;
  231. }
  232.  
  233. /*
  234.  *  taut_special_cases -- check special cases for tautology
  235.  */
  236.  
  237. bool
  238. taut_special_cases(T)
  239. pcube *T;            /* will be disposed if answer is determined */
  240. {
  241.     register pcube *T1, *Tsave, p, ceil=cube.temp[0], temp=cube.temp[1];
  242.     pcube *A, *B;
  243.     int var;
  244.  
  245.     /* Check for a row of all 1's which implies tautology */
  246.     for(T1 = T+2; (p = *T1++) != NULL; ) {
  247.     if (full_row(p, T[0])) {
  248.         free_cubelist(T);
  249.         return TRUE;
  250.     }
  251.     }
  252.  
  253.     /* Check for a column of all 0's which implies no tautology */
  254. start:
  255.     INLINEset_copy(ceil, T[0]);
  256.     for(T1 = T+2; (p = *T1++) != NULL; ) {
  257.     INLINEset_or(ceil, ceil, p);
  258.     }
  259.     if (! setp_equal(ceil, cube.fullset)) {
  260.     free_cubelist(T);
  261.     return FALSE;
  262.     }
  263.  
  264.     /* Collect column counts, determine unate variables, etc. */
  265.     massive_count(T);
  266.  
  267.     /* If function is unate (and no row of all 1's), then no tautology */
  268.     if (cdata.vars_unate == cdata.vars_active) {
  269.     free_cubelist(T);
  270.     return FALSE;
  271.  
  272.     /* If active in a single variable (and no column of 0's) then tautology */
  273.     } else if (cdata.vars_active == 1) {
  274.     free_cubelist(T);
  275.     return TRUE;
  276.  
  277.     /* Check for unate variables, and reduce cover if there are any */
  278.     } else if (cdata.vars_unate != 0) {
  279.     /* Form a cube "ceil" with full variables in the unate variables */
  280.     (void) set_copy(ceil, cube.emptyset);
  281.     for(var = 0; var < cube.num_vars; var++) {
  282.         if (cdata.is_unate[var]) {
  283.         INLINEset_or(ceil, ceil, cube.var_mask[var]);
  284.         }
  285.     }
  286.  
  287.     /* Save only those cubes that are "full" in all unate variables */
  288.     for(Tsave = T1 = T+2; (p = *T1++) != 0; ) {
  289.         if (setp_implies(ceil, set_or(temp, p, T[0]))) {
  290.         *Tsave++ = p;
  291.         }
  292.     }
  293.     *Tsave++ = NULL;
  294.     T[1] = (pcube) Tsave;
  295.  
  296.     if (debug & TAUT) {
  297.         printf("UNATE_REDUCTION: %d unate variables, reduced to %d\n",
  298.         cdata.vars_unate, CUBELISTSIZE(T));
  299.     }
  300.     goto start;
  301.  
  302.     /* Check for component reduction */
  303.     } else if (cdata.var_zeros[cdata.best] < CUBELISTSIZE(T) / 2) {
  304.     if (cubelist_partition(T, &A, &B, debug & TAUT) == 0) {
  305.         return MAYBE;
  306.     } else {
  307.         free_cubelist(T);
  308.         if (tautology(A)) {
  309.         free_cubelist(B);
  310.         return TRUE;
  311.         } else {
  312.         return tautology(B);
  313.         }
  314.     }
  315.     }
  316.  
  317.     /* We tried as hard as we could, but must recurse from here on */
  318.     return MAYBE;
  319. }
  320.  
  321. /* fcube_is_covered -- determine exactly how a cubelist "covers" a cube */
  322. static void
  323. fcube_is_covered(T, c, table)
  324. pcube *T, c;
  325. sm_matrix *table;
  326. {
  327.     ftautology(cofactor(T,c), table);
  328. }
  329.  
  330.  
  331. /* ftautology -- find ways to make a tautology */
  332. static void
  333. ftautology(T, table)
  334. pcube *T;             /* T will be disposed of */
  335. sm_matrix *table;
  336. {
  337.     register pcube cl, cr;
  338.     register int best;
  339.     static int ftaut_level = 0;
  340.  
  341.     if (debug & TAUT) {
  342.     debug_print(T, "FIND_TAUTOLOGY", ftaut_level++);
  343.     }
  344.  
  345.     if (ftaut_special_cases(T, table) == MAYBE) {
  346.     cl = new_cube();
  347.     cr = new_cube();
  348.     best = binate_split_select(T, cl, cr, TAUT);
  349.  
  350.     ftautology(scofactor(T, cl, best), table);
  351.     ftautology(scofactor(T, cr, best), table);
  352.  
  353.     free_cubelist(T);
  354.     free_cube(cl);
  355.     free_cube(cr);
  356.     }
  357.  
  358.     if (debug & TAUT) {
  359.     (void) printf("exit FIND_TAUTOLOGY[%d]: table is %d by %d\n",
  360.         --ftaut_level, table->nrows, table->ncols);
  361.     }
  362. }
  363.  
  364. static bool
  365. ftaut_special_cases(T, table)
  366. pcube *T;                 /* will be disposed if answer is determined */
  367. sm_matrix *table;
  368. {
  369.     register pcube *T1, *Tsave, p, temp = cube.temp[0], ceil = cube.temp[1];
  370.     int var, rownum;
  371.  
  372.     /* Check for a row of all 1's in the essential cubes */
  373.     for(T1 = T+2; (p = *T1++) != 0; ) {
  374.     if (! TESTP(p, REDUND)) {
  375.         if (full_row(p, T[0])) {
  376.         /* subspace is covered by essentials -- no new rows for table */
  377.         free_cubelist(T);
  378.         return TRUE;
  379.         }
  380.     }
  381.     }
  382.  
  383.     /* Collect column counts, determine unate variables, etc. */
  384. start:
  385.     massive_count(T);
  386.  
  387.     /* If function is unate, find the rows of all 1's */
  388.     if (cdata.vars_unate == cdata.vars_active) {
  389.     /* find which nonessentials cover this subspace */
  390.     rownum = table->last_row ? table->last_row->row_num+1 : 0;
  391.     (void) sm_insert(table, rownum, Rp_current);
  392.     for(T1 = T+2; (p = *T1++) != 0; ) {
  393.         if (TESTP(p, REDUND)) {
  394.         /* See if a redundant cube covers this leaf */
  395.         if (full_row(p, T[0])) {
  396.             (void) sm_insert(table, rownum, (int) SIZE(p));
  397.         }
  398.         }
  399.     }
  400.     free_cubelist(T);
  401.     return TRUE;
  402.  
  403.     /* Perform unate reduction if there are any unate variables */
  404.     } else if (cdata.vars_unate != 0) {
  405.     /* Form a cube "ceil" with full variables in the unate variables */
  406.     (void) set_copy(ceil, cube.emptyset);
  407.     for(var = 0; var < cube.num_vars; var++) {
  408.         if (cdata.is_unate[var]) {
  409.         INLINEset_or(ceil, ceil, cube.var_mask[var]);
  410.         }
  411.     }
  412.  
  413.     /* Save only those cubes that are "full" in all unate variables */
  414.     for(Tsave = T1 = T+2; (p = *T1++) != 0; ) {
  415.         if (setp_implies(ceil, set_or(temp, p, T[0]))) {
  416.         *Tsave++ = p;
  417.         }
  418.     }
  419.     *Tsave++ = 0;
  420.     T[1] = (pcube) Tsave;
  421.  
  422.     if (debug & TAUT) {
  423.         printf("UNATE_REDUCTION: %d unate variables, reduced to %d\n",
  424.         cdata.vars_unate, CUBELISTSIZE(T));
  425.     }
  426.     goto start;
  427.     }
  428.  
  429.     /* Not much we can do about it */
  430.     return MAYBE;
  431. }
  432.